These are archival webpages, generated on 2023-03-20 by Prove-It Beta Version 0.3, licensed under the GNU Public Licence by Sandia Corporation. See pyproveit.org for the lastest version.
logo

Proof of proveit.physics.quantum.QPE._psi_t_var_formula theorem

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, c, k, m, n, t, P, defaults, Function
from proveit.linear_algebra import ScalarMult, TensorProd
from proveit.logic import Equals, InSet
from proveit.numbers import (
        zero, one, two, i, e, pi, Add, Exp, Less, LessEq, Mult, Neg, subtract)
from proveit.numbers import Complex, Interval, Natural
from proveit.numbers.exponentiation import (
        add_one_right_in_exp, exp_eq_for_eq_base_and_exp, exponential_monotonocity)
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural_pos
from proveit.physics.quantum import Ket
from proveit.physics.quantum.QPE import _phase, _phase_is_real, _psi_t_def
In [2]:
%proving _psi_t_var_formula
Out[2]:
Under these presumptions, we begin our proof of
_psi_t_var_formula:
(see dependencies)
In [3]:
defaults.assumptions = _psi_t_var_formula.all_conditions()
Out[3]:
defaults.assumptions:
In [4]:
# the induction theorem for positive naturals
fold_forall_natural_pos
Out[4]:
 ⊢  
In [5]:
# instantiate the induction theorem
induction_inst = fold_forall_natural_pos.instantiate(
    {Function(P,t):_psi_t_var_formula.instance_expr, m:t, n:t})
Out[5]:
induction_inst:  ⊢  

Mainly: some domains and orderings. Notice that throughout this section devoted to the induction proof, $t$ is a variable, not a literal.

In [6]:
# used when processing products involving the phase phi
_phase_is_real
Out[6]:
 ⊢  
In [7]:
two_pow_t_var_less_one = subtract(Exp(two, t), one)
Out[7]:
two_pow_t_var_less_one:
In [8]:
two_pow_t_var_less_one.deduce_in_number_set(Natural)
Out[8]:
 ⊢  
In [9]:
LessEq(zero, two_pow_t_var_less_one).prove()
Out[9]:
 ⊢  
In [10]:
Less(t, Add(t, one)).prove()
Out[10]:
 ⊢  
In [11]:
exponential_monotonocity
Out[11]:
 ⊢  
In [12]:
exponential_monotonocity_inst = exponential_monotonocity.instantiate({a: two, b: t, c: Add(t, one)})
Out[12]:
exponential_monotonocity_inst:  ⊢  
In [13]:
# Used to allow a splitting of a summation into the sum of two summations
exponential_monotonocity_inst.derive_shifted(Neg(one))
Out[13]:
 ⊢  

Base Case

In [14]:
base_case = induction_inst.antecedent.operands[0]
Out[14]:
base_case:

We have $|\psi_{t}\rangle$ defined as a tensor product (the result of the first phase of the quantum circuit, and the LHS of Nielsen & Chuang's identity 5.20 on pg 222):

In [15]:
_psi_t_def
Out[15]:
 ⊢  
In [16]:
_psi_t_as_tensor_prod = _psi_t_def.instantiate()
Out[16]:
_psi_t_as_tensor_prod:  ⊢  

For $\psi'_{1}$, we prove a useful equality then instantiate the psi_t_def with $t=1$:

In [17]:
psi_1_def = _psi_t_def.instantiate({t:one})
Out[17]:
psi_1_def:  ⊢  

Then show that the summation formula also gives the same qbit result

In [18]:
sum_0_to_1 = base_case.rhs
Out[18]:
sum_0_to_1:
In [19]:
sum_0_to_1_processed_01 = sum_0_to_1.inner_expr().operands[1].partitioning_first()
Out[19]:
sum_0_to_1_processed_01:  ⊢  
In [20]:
# finish off the Base Case
base_case_jdgmt = sum_0_to_1_processed_01.sub_left_side_into(psi_1_def)
Out[20]:
base_case_jdgmt:  ⊢  

Inductive Step

In [21]:
inductive_step = induction_inst.antecedent.operands[1]
Out[21]:
inductive_step:
In [22]:
defaults.assumptions = defaults.assumptions + inductive_step.conditions.entries
Out[22]:
defaults.assumptions:
In [23]:
# for convenience for later
scalar_coeff = inductive_step.instance_expr.rhs.scalar
Out[23]:
scalar_coeff:

First, partition the summation: $\sum_{k=0}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} = \sum_{k=0}^{2^{t}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} + \sum_{k=2^{t}}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1}$

In [24]:
summation_partition_01 = (
    inductive_step.instance_expr.rhs.operands[1]
    .partitioning(two_pow_t_var_less_one))
Out[24]:
summation_partition_01:  ⊢  

Then shift the second summation of that partition, so that the two summations then have the same index domain:

In [25]:
summation_partition_02 = (summation_partition_01.inner_expr().rhs.
                          operands[1].shift(Neg(Exp(two, t))))
Out[25]:
summation_partition_02:  ⊢  
In [26]:
summation_partition_02.inner_expr().rhs.operands[1].domain.upper_bound.operands[0]
Out[26]:
In [27]:
from proveit.numbers import deduce_number_set
summation_partition_02.rhs.operands[1].domain.upper_bound.simplification()
Out[27]:
 ⊢  
In [28]:
deduce_number_set(summation_partition_02.rhs.operands[1].domain.upper_bound)
Out[28]:
 ⊢  
In [29]:
summation_partition_03 = (summation_partition_02.inner_expr().rhs.
        operands[1].domain.upper_bound.operands[0].exponent_separate())
Out[29]:
summation_partition_03:  ⊢  

We want to rewrite the summand of that 2nd summation on the rhs now by (1) expanding the exponential term and (2) rewriting the $|k+2^t{\rangle}_{t+1}$ ket as $|1\rangle \otimes |k{\rangle}_t$. This takes a little work.

In [30]:
rhs_2nd_sum = summation_partition_03.rhs.operands[1]
Out[30]:
rhs_2nd_sum:
In [31]:
summand_processed_01 = rhs_2nd_sum.summand.inner_expr().operands[0].exponent.distribution(
    4, assumptions=[*defaults.assumptions,
                    rhs_2nd_sum.condition])
Out[31]:
summand_processed_01: ,  ⊢  
In [32]:
summand_processed_02 = (
    summand_processed_01.inner_expr().rhs.operands[0]
    .exponent_separate(
        assumptions=[*defaults.assumptions,
                     InSet(k, Interval(zero, subtract(Exp(two, t), one)))]))
Out[32]:
summand_processed_02: ,  ⊢  
In [33]:
# Avoid recombine these via auto-simplification
defaults.preserved_exprs = set([summand_processed_02.rhs.scalar])
Out[33]:
defaults.preserved_exprs:
In [34]:
# commute the NumKet num operands to format it for replacement later
# using the prepend_num_ket_with_one_ket theorem
summand_processed_03 = summand_processed_02.inner_expr().rhs.operands[1].num.commute(
    assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
Out[34]:
summand_processed_03: ,  ⊢  
In [35]:
from proveit.physics.quantum.algebra import prepend_num_ket_with_one_ket
prepend_num_ket_with_one_ket
Out[35]:
 ⊢  
In [36]:
prepend_num_ket_with_one_ket_inst = prepend_num_ket_with_one_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
Out[36]:
prepend_num_ket_with_one_ket_inst: ,  ⊢  
In [37]:
summand_processed_04 = (
    summand_processed_03.inner_expr().rhs.operands[1]
    .substitute(prepend_num_ket_with_one_ket_inst))
Out[37]:
summand_processed_04: ,  ⊢  
In [38]:
# reminder of summation_partition_03
summation_partition_03
Out[38]:
 ⊢  
In [39]:
summation_partition_04 = (
    summation_partition_03.inner_expr().rhs.operands[1].summand.substitute(
        summand_processed_04))
Out[39]:
summation_partition_04:  ⊢  

Also process the summand in the 1st sum on the rhs, converting the ket $|k\rangle_{t+1}$ to the tensor product $|0\rangle \otimes |k\rangle_{t}$:

In [40]:
# pull up the relevant NumKet theorem
from proveit.physics.quantum.algebra import prepend_num_ket_with_zero_ket
prepend_num_ket_with_zero_ket
Out[40]:
 ⊢  
In [41]:
# instantiate the theorem for our specific case
prepend_num_ket_with_zero_ket_inst = prepend_num_ket_with_zero_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
Out[41]:
prepend_num_ket_with_zero_ket_inst: ,  ⊢  
In [42]:
# use our instantiation to substitute
summation_partition_05 = (
    summation_partition_04.inner_expr().rhs.operands[0].summand.scaled.substitute(
    prepend_num_ket_with_zero_ket_inst))
Out[42]:
summation_partition_05:  ⊢  

We also then want to:

(1) pull the tensor product out of the 2nd summation, and

(2) pull the non-$k$-dependent exponential factor out of the 2nd summation.

In [43]:
# for convenience:
temp_factors = summation_partition_04.rhs.operands[1].summand.operands[0]
Out[43]:
temp_factors:
In [44]:
# for convenience:
temp_factor_01 = temp_factors.operands[0]
Out[44]:
temp_factor_01:
In [45]:
# for convenience:
temp_factor_02 = temp_factors.operands[1]
Out[45]:
temp_factor_02:
In [46]:
# another convenience: an expr for the current domain of index k
k_domain = summation_partition_04.rhs.operands[1].conditions[0]
Out[46]:
k_domain:
In [47]:
from proveit.linear_algebra import VecSpaces
from proveit.numbers import Real
VecSpaces.default_field=Complex
summation_partition_06 = summation_partition_05.inner_expr().rhs.operands[1].factors_extract()
Out[47]:
summation_partition_06:  ⊢  
In [48]:
summation_partition_07 = (
    summation_partition_06.inner_expr().rhs.operands[0].factors_extract())

Found summation index k in the scalar e^{2 * pi * i * phase * k} and the scalar is not a Mult object.
Out[48]:
summation_partition_07:  ⊢  

Now factor out the common vector summation factor in the two terms of the rhs. We do this using our VecAdd.factorization() method after we quickly re-associate terms in the far right-hand side vector.

In [49]:
temp_summation = summation_partition_07.rhs.operands[1].scaled.operands[1]
desired_expr = TensorProd(ScalarMult(temp_factor_02, Ket(one)), temp_summation)
Out[49]:
desired_expr:
In [50]:
summation_partition_08 = (
    desired_expr.scalar_factorization(idx=0)
    .sub_left_side_into(summation_partition_07.inner_expr().rhs.operands[1]))
Out[50]:
summation_partition_08:  ⊢  

Now as promised we utilize the VecAdd.factorization() method. We need to let it know we're dealing with vectors over the field of Complex numbers and we want to “pull” the factor to the right:

In [51]:
temp_factor = summation_partition_08.rhs.operands[0].operands[1]
summation_partition_09 = summation_partition_08.inner_expr().rhs.factor(temp_factor, pull='right', field=Complex)
Out[51]:
summation_partition_09:  ⊢  

Reintroduce the scalar coefficient:

In [52]:
summation_partition_10 = inductive_step.instance_expr.rhs.inner_expr().scaled.substitution(summation_partition_09)
Out[52]:
summation_partition_10:  ⊢  

Manipulate our scalar coefficient in preparation for distribution a portion of it across the tensor product:

In [53]:
# recall
scalar_coeff
Out[53]:
In [54]:
scalar_coeff_02 = scalar_coeff.inner_expr().denominator.exponent.distribution()
Out[54]:
scalar_coeff_02:  ⊢  
In [55]:
scalar_coeff_03 = scalar_coeff_02.inner_expr().rhs.denominator.exponent_separate()
Out[55]:
scalar_coeff_03:  ⊢  
In [56]:
from proveit.numbers import frac
scalar_coeff_04 = scalar_coeff_03.inner_expr().rhs.factor(frac(one, Exp(two, frac(one, two))))
Out[56]:
scalar_coeff_04:  ⊢  
In [57]:
summation_partition_11 = summation_partition_10.inner_expr().rhs.scalar.substitute(scalar_coeff_04)
Out[57]:
summation_partition_11:  ⊢  
In [58]:
# represent the desired (distributed scalar-product) outcome:
desired_expr = (
    TensorProd(
        ScalarMult(frac(one, Exp(two, frac(one, two))), summation_partition_11.rhs.scaled.operands[0]),
        ScalarMult(frac(one, Exp(two, frac(t, two))), summation_partition_11.rhs.scaled.operands[1])
    ))
Out[58]:
desired_expr:
In [59]:
# let Prove-It prove the equality:
distrib_equality = Equals(summation_partition_11.rhs, desired_expr).prove()
Out[59]:
distrib_equality:  ⊢  
In [60]:
# now use that equality in our earlier work:
conclusion_01 = distrib_equality.sub_right_side_into(summation_partition_11)
Out[60]:
conclusion_01:  ⊢  
In [61]:
# Recall our inductive hypothesis:
for item in defaults.assumptions:
    if isinstance(item, Equals):
        inductive_hypothesis = item
inductive_hypothesis
Out[61]:
In [62]:
# use the inductive hypothesis:
conclusion_02 = inductive_hypothesis.sub_left_side_into(conclusion_01)
Out[62]:
conclusion_02: ,  ⊢  

The RHS of conclusion02 above should be equal to $|\psi{t+1}\rangle$. Let's see how to get there. Ideally we could use the next three cells to show the rhs of the equality in `conclusion_2` is equal to $|\psi_{t+1}\rangle$

In [63]:
# reminder
_psi_t_def
Out[63]:
 ⊢  
In [ ]:
In [ ]:
In [64]:
# from proveit.numbers import Add, Neg, one, NaturalPos
# from proveit import t, defaults
# from proveit.logic import InSet
# defaults.assumptions = [InSet(t, NaturalPos)]
# %begin
# Add(Neg(Add(t, one)), one)#.simplification()
In [65]:
# Add(Neg(Add(t, one)), one).simplification()
In [ ]:
In [66]:
psi_t_plus_one_as_tensor_prod = _psi_t_def.instantiate({t:Add(t, one)})
Out[66]:
psi_t_plus_one_as_tensor_prod:  ⊢  

The following three cell/steps needed so that the substitute step will be able to perform the desired simplification, pulling the coefficients out to the front:

In [67]:
from proveit.numbers import greater_eq, NaturalPos
t_greater_eq_one = greater_eq(t, one).prove()
Out[67]:
t_greater_eq_one:  ⊢  
In [68]:
t_minus_one_greater_eq_zero = t_greater_eq_one.right_add_both_sides(Neg(one))
Out[68]:
t_minus_one_greater_eq_zero:  ⊢  
In [69]:
t_minus_one_greater_eq_zero.derive_negated()
Out[69]:
 ⊢  

Now this substitute() step will also manage to pull the scalar coefficients out to the front in the process:

In [70]:
conclusion_03 = conclusion_02.inner_expr().rhs.operands[1].substitute(
        _psi_t_as_tensor_prod)
Out[70]:
conclusion_03: ,  ⊢  

Now we partition the tensor product expression of $\psi_{t+1}$, so we can eventually show that it is equal to the rhs of conclusion_03.

In [71]:
# to be used as a replacement in the partition step that follows
neg_t_plus_one_sub = Neg(Add(t, Neg(one))).distribution().derive_reversed()
Out[71]:
neg_t_plus_one_sub:  ⊢  
In [72]:
psi_t_plus_one_as_tensor_prod.rhs
Out[72]:
In [73]:
# from proveit import t, defaults
# from proveit.logic import InSet
# from proveit.numbers import deduce_number_set, NaturalPos, subtract, Neg, Add, one
# defaults.assumptions = [InSet(t, NaturalPos)]
# %begin
# deduce_number_set(
#     subtract(Add(Neg(Neg(t)), one), Add(Neg(t), one)).simplification().rhs)
In [74]:
neg_t_plus_one_sub
Out[74]:
 ⊢  
In [75]:
# # needed explicitly(somewhat oddly) for the next step of substitution
Add(t, one).commutation()
Out[75]:
 ⊢  
In [76]:
# # we can partition the operands in the psi_{t+1} tensor prod expression
psi_t_plus_one_as_tensor_prod_02 = (
    psi_t_plus_one_as_tensor_prod.inner_expr().rhs.operands[0].split(t))
Out[76]:
psi_t_plus_one_as_tensor_prod_02:  ⊢  
In [77]:
conclusion_04 = conclusion_03.inner_expr().rhs.scaled.factors[0].terms[1].scalar.exponent.commute(3, 4)
Out[77]:
conclusion_04: ,  ⊢  
In [78]:
conclusion_04.inner_expr().rhs.substitute(psi_t_plus_one_as_tensor_prod_02.derive_reversed())
Out[78]:
,  ⊢  
In [79]:
# # recall our earlier instantiation of the induction theorem:
induction_inst
Out[79]:
 ⊢  

We have proven both pieces of the antecedent (i.e., the base case and inductive case) of the instantiated induction theorem induction_inst, so we can now derive the consequent:

In [80]:
induction_inst.derive_consequent()

_psi_t_var_formula has been proven.  Now simply execute "%qed".
Out[80]:
 ⊢  
In [81]:
%qed
Out[81]:
 step typerequirementsstatement
0modus ponens1, 2  ⊢  
1instantiation3, 4*, 5*  ⊢  
  : , : , :
2instantiation6, 7, 8  ⊢  
  : , :
3conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4instantiation370, 9, 430  ⊢  
  : , : , :
5instantiation10, 11  ⊢  
  :
6theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
7instantiation432, 12, 13  ⊢  
  : , : , :
8generalization14  ⊢  
9instantiation459, 423  ⊢  
  : , : , :
10conjecture  ⊢  
 proveit.physics.quantum.algebra.single_qubit_num_ket
11instantiation15, 16, 17  ⊢  
  :
12instantiation73, 558, 18, 19*  ⊢  
  :
13instantiation459, 20  ⊢  
  : , : , :
14instantiation425, 21,  ⊢  
  : , :
15conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
16instantiation559, 22, 24  ⊢  
  : , : , :
17instantiation23, 543, 537, 24  ⊢  
  : , : , :
18instantiation401, 290, 25  ⊢  
  : , : , :
19instantiation370, 26, 27  ⊢  
  : , : , :
20instantiation28, 543, 537, 29, 30*, 31*  ⊢  
  : , : , : , :
21instantiation432, 32, 33,  ⊢  
  : , : , :
22instantiation542, 543, 537  ⊢  
  : , :
23conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
24assumption  ⊢  
25instantiation435, 456, 429  ⊢  
  : , :
26instantiation459, 34  ⊢  
  : , : , :
27instantiation35, 442, 36  ⊢  
  : , : , :
28conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_split_first
29conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
30instantiation370, 37, 38  ⊢  
  : , : , :
31instantiation370, 39, 40  ⊢  
  : , : , :
32instantiation401, 41, 42,  ⊢  
  : , : , :
33instantiation43, 490, 44, 80, 45, 46, 47*  ⊢  
  : , : , : , :
34instantiation370, 48, 49  ⊢  
  : , : , :
35axiom  ⊢  
 proveit.linear_algebra.tensors.unary_tensor_prod_def
36instantiation443, 442, 201, 50  ⊢  
  : , : , : , :
37instantiation459, 51  ⊢  
  : , : , :
38instantiation52, 456, 282, 442  ⊢  
  : , : , :
39instantiation459, 317  ⊢  
  : , : , :
40instantiation53, 537, 54*  ⊢  
  : , :
41instantiation401, 55, 56, 57*,  ⊢  
  : , : , :
42instantiation58, 353, 427, 546, 66, 479, 502, 503, 504, 505, 481  ⊢  
  : , : , : , : , : , : , :
43conjecture  ⊢  
 proveit.logic.equality.sub_in_right_operands_via_tuple
44instantiation370, 59, 151  ⊢  
  : , : , :
45instantiation73, 511, 60  ⊢  
  :
46instantiation61, 62, 311*  ⊢  
  : , : , :
47modus ponens63, 64  ⊢  
48instantiation459, 65  ⊢  
  : , : , :
49instantiation70, 353, 427, 66, 502, 503, 504, 505  ⊢  
  : , : , : , :
50instantiation236, 442, 282, 67  ⊢  
  : , : , : , :
51instantiation370, 68, 69  ⊢  
  : , : , :
52conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.one_as_scalar_mult_id
53axiom  ⊢  
 proveit.linear_algebra.addition.vec_sum_single
54instantiation70, 476, 546, 477, 479, 502, 503, 504, 505  ⊢  
  : , : , : , :
55instantiation432, 71, 72,  ⊢  
  : , : , :
56instantiation73, 561  ⊢  
  :
57instantiation370, 74, 75  ⊢  
  : , : , :
58conjecture  ⊢  
 proveit.numbers.multiplication.rightward_commutation
59instantiation401, 76, 114  ⊢  
  : , : , :
60instantiation370, 77, 78  ⊢  
  : , : , :
61conjecture  ⊢  
 proveit.core_expr_types.tuples.partition_front
62instantiation432, 556, 79  ⊢  
  : , : , :
63instantiation409, 201, 546, 556, 112, 479, 127  ⊢  
  : , : , : , : , : , : , : , :
64instantiation437, 129, 175, 130, 442, 146, 80, 81, 128  ⊢  
  : , : , : , :
65instantiation370, 82, 83  ⊢  
  : , : , :
66instantiation385  ⊢  
  : , : , :
67instantiation443, 442, 84, 439  ⊢  
  : , : , : , :
68instantiation459, 85  ⊢  
  : , : , :
69instantiation100, 86  ⊢  
  :
70conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_any
71instantiation432, 87, 88  ⊢  
  : , : , :
72assumption  ⊢  
73axiom  ⊢  
 proveit.physics.quantum.QPE._psi_t_def
74modus ponens89, 90  ⊢  
75modus ponens91, 92  ⊢  
76instantiation221, 93  ⊢  
  : , : , :
77instantiation94, 546, 555, 427, 479, 420, 422, 456  ⊢  
  : , : , : , : , : , :
78instantiation394, 456, 310  ⊢  
  : , :
79instantiation370, 95, 96  ⊢  
  : , : , :
80instantiation370, 97, 151  ⊢  
  : , : , :
81instantiation443, 442, 201, 98  ⊢  
  : , : , : , :
82instantiation459, 99  ⊢  
  : , : , :
83instantiation100, 502  ⊢  
  :
84instantiation559, 465, 101  ⊢  
  : , : , :
85instantiation102, 476, 546, 477, 479, 502, 503, 504, 505  ⊢  
  : , : , : , :
86instantiation559, 521, 103  ⊢  
  : , : , :
87instantiation401, 104, 105  ⊢  
  : , : , :
88modus ponens106, 107  ⊢  
89instantiation108, 427, 222, 546, 109, 240, 127, 479  ⊢  
  : , : , : , : , : , : , : , :
90instantiation437, 538, 125, 442, 126, 110, 124, 111  ⊢  
  : , : , : , :
91instantiation409, 201, 546, 556, 112, 479, 127  ⊢  
  : , : , : , : , : , : , : , :
92instantiation437, 129, 175, 130, 442, 146, 113, 124, 128  ⊢  
  : , : , : , :
93instantiation432, 490, 114  ⊢  
  : , : , :
94conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtraction_disassociation
95instantiation459, 311  ⊢  
  : , : , :
96instantiation115, 422  ⊢  
  :
97instantiation370, 116, 175  ⊢  
  : , : , :
98instantiation236, 442, 282, 117  ⊢  
  : , : , : , :
99conjecture  ⊢  
 proveit.numbers.negation.negated_zero
100conjecture  ⊢  
 proveit.numbers.exponentiation.exp_zero_eq_one
101instantiation482, 483, 118  ⊢  
  : , :
102conjecture  ⊢  
 proveit.numbers.multiplication.mult_zero_any
103instantiation559, 528, 516  ⊢  
  : , : , :
104instantiation459, 119  ⊢  
  : , : , :
105instantiation401, 120, 121  ⊢  
  : , : , :
106instantiation409, 201, 546, 427, 410, 479, 122*  ⊢  
  : , : , : , : , : , : , : , :
107instantiation437, 538, 441, 442, 444, 123, 124, 220  ⊢  
  : , : , : , :
108conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_disassociation
109instantiation440, 538, 125, 442, 126  ⊢  
  : , : , :
110instantiation495  ⊢  
  : , :
111instantiation437, 144, 240, 145, 146, 127, 128  ⊢  
  : , : , : , :
112instantiation440, 129, 175, 130, 442, 146  ⊢  
  : , : , :
113instantiation370, 131, 151  ⊢  
  : , : , :
114instantiation370, 132, 133  ⊢  
  : , : , :
115conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
116instantiation203, 538, 134, 205, 206, 207, 222, 228*, 240*  ⊢  
  : , : , : , :
117instantiation443, 442, 135, 439  ⊢  
  : , : , : , :
118instantiation499, 476, 477, 502, 503, 504, 505  ⊢  
  : , :
119instantiation432, 136, 137  ⊢  
  : , : , :
120instantiation432, 138, 139  ⊢  
  : , : , :
121instantiation370, 140, 141  ⊢  
  : , : , :
122instantiation370, 142, 143  ⊢  
  : , : , :
123instantiation495  ⊢  
  : , :
124instantiation443, 442, 201, 219  ⊢  
  : , : , : , :
125instantiation495  ⊢  
  : , :
126instantiation440, 144, 240, 145, 146  ⊢  
  : , : , :
127instantiation370, 147, 168  ⊢  
  : , : , :
128modus ponens148, 149  ⊢  
129instantiation526, 558, 561  ⊢  
  : , :
130instantiation370, 150, 151  ⊢  
  : , : , :
131instantiation370, 152, 175  ⊢  
  : , : , :
132instantiation459, 311  ⊢  
  : , : , :
133instantiation352, 546, 555, 479, 420, 422, 456  ⊢  
  : , : , : , :
134instantiation495  ⊢  
  : , :
135instantiation559, 465, 153  ⊢  
  : , : , :
136instantiation432, 154, 155  ⊢  
  : , : , :
137modus ponens156, 165  ⊢  
138instantiation459, 157  ⊢  
  : , : , :
139instantiation461, 538, 158, 421, 159, 160  ⊢  
  : , : , :
140instantiation459, 161  ⊢  
  : , : , :
141instantiation425, 162  ⊢  
  : , :
142instantiation459, 163  ⊢  
  : , : , :
143instantiation164, 410, 165, 201, 238, 166*  ⊢  
  : , : , : , : , :
144instantiation432, 561, 240  ⊢  
  : , : , :
145instantiation370, 167, 168  ⊢  
  : , : , :
146instantiation169, 532, 543, 442, 172  ⊢  
  : , : , :
147instantiation401, 170, 240  ⊢  
  : , : , :
148instantiation171, 532, 543, 172  ⊢  
  : , : , : , :
149generalization173  ⊢  
150instantiation370, 174, 175  ⊢  
  : , : , :
151instantiation425, 176  ⊢  
  : , :
152instantiation203, 538, 177, 205, 206, 207, 222, 228*, 240*  ⊢  
  : , : , : , :
153instantiation482, 483, 178  ⊢  
  : , :
154instantiation432, 179, 180  ⊢  
  : , : , :
155modus ponens181, 182  ⊢  
156instantiation183, 546, 555, 427, 410, 479, 184  ⊢  
  : , : , : , : , : , : , : , :
157instantiation185, 538, 420, 422, 456, 502, 186  ⊢  
  : , : , :
158instantiation495  ⊢  
  : , :
159instantiation559, 521, 414  ⊢  
  : , : , :
160instantiation559, 521, 187  ⊢  
  : , : , :
161instantiation424, 188, 189  ⊢  
  : , :
162instantiation190, 456, 191, 192, 193*  ⊢  
  : , : , : , :
163modus ponens194, 195  ⊢  
164conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled
165instantiation437, 538, 441, 442, 444, 196, 219, 239  ⊢  
  : , : , : , :
166instantiation197, 201, 238  ⊢  
  : , :
167instantiation401, 198, 240  ⊢  
  : , : , :
168instantiation425, 199  ⊢  
  : , :
169conjecture  ⊢  
 proveit.logic.booleans.conjunction.redundant_conjunction_general
170instantiation221, 222  ⊢  
  : , : , :
171conjecture  ⊢  
 proveit.logic.booleans.conjunction.conjunction_from_quantification
172instantiation432, 200, 317  ⊢  
  : , : , :
173instantiation443, 442, 201, 202,  ⊢  
  : , : , : , :
174instantiation203, 538, 204, 205, 206, 207, 222, 228*, 240*  ⊢  
  : , : , : , :
175instantiation435, 456, 422  ⊢  
  : , :
176instantiation223, 490  ⊢  
  : , :
177instantiation495  ⊢  
  : , :
178instantiation499, 500, 208, 502, 503, 504, 481, 505  ⊢  
  : , :
179instantiation401, 209, 210  ⊢  
  : , : , :
180modus ponens211, 212  ⊢  
181instantiation409, 406, 546, 427, 410, 479  ⊢  
  : , : , : , : , : , : , : , :
182instantiation437, 538, 441, 442, 444, 213, 237, 239  ⊢  
  : , : , : , :
183conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_distribution_over_add
184instantiation495  ⊢  
  : , :
185conjecture  ⊢  
 proveit.numbers.division.distribute_frac_through_sum
186instantiation214, 538  ⊢  
  :
187instantiation559, 530, 215  ⊢  
  : , : , :
188instantiation559, 521, 216  ⊢  
  : , : , :
189instantiation559, 521, 217  ⊢  
  : , : , :
190conjecture  ⊢  
 proveit.numbers.division.prod_of_fracs
191instantiation559, 497, 288  ⊢  
  : , : , :
192instantiation559, 497, 348  ⊢  
  : , : , :
193instantiation458, 456  ⊢  
  :
194instantiation409, 238, 427, 546, 410, 479  ⊢  
  : , : , : , : , : , : , : , :
195instantiation437, 538, 441, 442, 444, 218, 219, 220  ⊢  
  : , : , : , :
196instantiation495  ⊢  
  : , :
197axiom  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
198instantiation221, 222  ⊢  
  : , : , :
199instantiation223, 556  ⊢  
  : , :
200instantiation224, 427, 546, 479, 225, 474  ⊢  
  : , : , : , : , :
201instantiation559, 521, 226  ⊢  
  : , : , :
202instantiation236, 442, 282, 227,  ⊢  
  : , : , : , :
203conjecture  ⊢  
 proveit.core_expr_types.tuples.general_len
204instantiation495  ⊢  
  : , :
205instantiation495  ⊢  
  : , :
206instantiation495  ⊢  
  : , :
207instantiation432, 427, 228  ⊢  
  : , : , :
208instantiation517  ⊢  
  : , : , : , : , :
209instantiation247, 229, 230  ⊢  
  : , :
210instantiation370, 231, 232  ⊢  
  : , : , :
211instantiation344, 427, 558, 546, 410, 479, 233*  ⊢  
  : , : , : , : , : , : , : , : , : , : , :
212generalization234  ⊢  
213instantiation495  ⊢  
  : , :
214conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
215instantiation559, 468, 235  ⊢  
  : , : , :
216instantiation559, 528, 383  ⊢  
  : , : , :
217instantiation559, 528, 314  ⊢  
  : , : , :
218instantiation495  ⊢  
  : , :
219instantiation236, 442, 282, 237  ⊢  
  : , : , : , :
220instantiation443, 444, 238, 239  ⊢  
  : , : , : , :
221conjecture  ⊢  
 proveit.core_expr_types.tuples.range_len
222instantiation432, 556, 240  ⊢  
  : , : , :
223conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len
224conjecture  ⊢  
 proveit.numbers.addition.term_as_weak_upper_bound
225instantiation559, 241, 242  ⊢  
  : , : , :
226instantiation559, 528, 243  ⊢  
  : , : , :
227instantiation443, 442, 244, 439,  ⊢  
  : , : , : , :
228instantiation329, 546, 555, 427, 479, 245, 456, 429, 246*  ⊢  
  : , : , : , : , : , :
229instantiation247, 248, 249  ⊢  
  : , :
230instantiation459, 250, 251*, 252*  ⊢  
  : , : , :
231instantiation370, 253, 254  ⊢  
  : , : , :
232instantiation459, 255, 378*  ⊢  
  : , : , :
233modus ponens256, 257,  ⊢  
234instantiation443, 410, 445, 258,  ⊢  
  : , : , : , :
235instantiation485, 346, 487  ⊢  
  : , :
236conjecture  ⊢  
 proveit.linear_algebra.addition.binary_closure
237instantiation443, 442, 406, 439  ⊢  
  : , : , : , :
238instantiation559, 521, 259  ⊢  
  : , : , :
239modus ponens260, 261  ⊢  
240instantiation370, 262, 263  ⊢  
  : , : , :
241conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonpos_within_real_nonpos
242instantiation559, 264, 265  ⊢  
  : , : , :
243instantiation306, 307, 314, 266  ⊢  
  : , :
244instantiation559, 465, 267,  ⊢  
  : , : , :
245instantiation495  ⊢  
  : , :
246instantiation370, 268, 317  ⊢  
  : , : , :
247theorem  ⊢  
 proveit.logic.equality.rhs_via_equality
248instantiation401, 269, 369, 270*  ⊢  
  : , : , :
249instantiation459, 271, 272*, 273*  ⊢  
  : , : , :
250modus ponens274, 275  ⊢  
251instantiation339, 540  ⊢  
  : , :
252instantiation339, 540  ⊢  
  : , :
253instantiation370, 276, 277  ⊢  
  : , : , :
254instantiation425, 278  ⊢  
  : , :
255instantiation425, 279  ⊢  
  : , :
256instantiation409, 445, 427, 546, 410, 479,  ⊢  
  : , : , : , : , : , : , : , :
257instantiation437, 538, 441, 442, 444, 280, 282, 412,  ⊢  
  : , : , : , :
258instantiation437, 538, 441, 442, 444, 281, 282, 446,  ⊢  
  : , : , : , :
259instantiation559, 528, 283  ⊢  
  : , : , :
260instantiation379, 558, 444  ⊢  
  : , : , : , : , : , :
261generalization412  ⊢  
262instantiation459, 284  ⊢  
  : , : , :
263instantiation370, 285, 286  ⊢  
  : , : , :
264conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonpos_int_within_rational_nonpos
265instantiation559, 287, 541  ⊢  
  : , : , :
266instantiation347, 288  ⊢  
  :
267instantiation482, 483, 289,  ⊢  
  : , :
268instantiation459, 290  ⊢  
  : , : , :
269instantiation401, 291, 292  ⊢  
  : , : , :
270instantiation370, 293, 294  ⊢  
  : , : , :
271modus ponens295, 296  ⊢  
272instantiation339, 540  ⊢  
  : , :
273instantiation339, 540  ⊢  
  : , :
274instantiation376, 558  ⊢  
  : , : , : , : , : , : , :
275generalization297  ⊢  
276instantiation459, 298, 299*, 301*  ⊢  
  : , : , :
277instantiation459, 300, 301*, 302*  ⊢  
  : , : , :
278modus ponens303, 304  ⊢  
279modus ponens305, 343  ⊢  
280instantiation495  ⊢  
  : , :
281instantiation495  ⊢  
  : , :
282conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_zero_in_qubit_space
283instantiation306, 307, 383, 308  ⊢  
  : , :
284instantiation309, 310, 456, 311*  ⊢  
  : , :
285instantiation370, 312, 313  ⊢  
  : , : , :
286instantiation394, 456, 422  ⊢  
  : , :
287conjecture  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_nonpos_int
288instantiation559, 515, 314  ⊢  
  : , : , :
289instantiation499, 500, 315, 502, 503, 504, 316, 505,  ⊢  
  : , :
290instantiation455, 351, 456, 317  ⊢  
  : , : , :
291instantiation318, 543, 544, 323, 319, 320, 321*  ⊢  
  : , : , : , : , :
292instantiation322, 548, 323, 324, 325*, 326*, 327*  ⊢  
  : , : , : , : , :
293instantiation328, 427, 546, 479, 331, 429, 366  ⊢  
  : , : , : , : , : , : , :
294instantiation329, 546, 555, 427, 479, 330, 331, 366, 429, 332*  ⊢  
  : , : , : , : , : , :
295instantiation376, 558  ⊢  
  : , : , : , : , : , : , :
296generalization333  ⊢  
297instantiation334, 561, 540,  ⊢  
  : , :
298modus ponens335, 336  ⊢  
299instantiation339, 540  ⊢  
  : , :
300modus ponens337, 338  ⊢  
301instantiation339, 540  ⊢  
  : , :
302instantiation339, 540  ⊢  
  : , :
303instantiation340, 558, 410, 341  ⊢  
  : , : , : , : , : , : , : , :
304modus ponens342, 343  ⊢  
305instantiation344, 427, 558, 546, 410, 479, 345*  ⊢  
  : , : , : , : , : , : , : , : , : , : , :
306conjecture  ⊢  
 proveit.numbers.division.div_real_pos_closure
307instantiation559, 450, 346  ⊢  
  : , : , :
308instantiation347, 348  ⊢  
  :
309conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
310instantiation559, 521, 349  ⊢  
  : , : , :
311instantiation367, 422  ⊢  
  :
312instantiation392, 427, 555, 350, 351, 422, 429, 456  ⊢  
  : , : , : , : , : , :
313instantiation352, 546, 353, 479, 354, 422, 429, 456  ⊢  
  : , : , : , :
314instantiation355, 421  ⊢  
  :
315instantiation517  ⊢  
  : , : , : , : , :
316instantiation559, 521, 356,  ⊢  
  : , : , :
317conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_0_1
318conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_split_after
319instantiation357, 358  ⊢  
  : , :
320instantiation359, 496, 396, 454, 360  ⊢  
  : , : , :
321instantiation370, 361, 362  ⊢  
  : , : , :
322conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_index_shift
323instantiation547, 449, 549  ⊢  
  : , :
324instantiation559, 552, 363  ⊢  
  : , : , :
325instantiation364, 481  ⊢  
  :
326instantiation392, 546, 555, 427, 479, 365, 368, 429, 366  ⊢  
  : , : , : , : , : , :
327instantiation367, 481  ⊢  
  :
328conjecture  ⊢  
 proveit.numbers.addition.leftward_commutation
329conjecture  ⊢  
 proveit.numbers.addition.association
330instantiation495  ⊢  
  : , :
331instantiation401, 368, 369  ⊢  
  : , : , :
332instantiation370, 371, 372  ⊢  
  : , : , :
333instantiation401, 373, 374,  ⊢  
  : , : , :
334conjecture  ⊢  
 proveit.physics.quantum.algebra.prepend_num_ket_with_zero_ket
335instantiation376, 558  ⊢  
  : , : , : , : , : , : , :
336generalization375  ⊢  
337instantiation376, 558  ⊢  
  : , : , : , : , : , : , :
338generalization377  ⊢  
339conjecture  ⊢  
 proveit.core_expr_types.conditionals.satisfied_condition_reduction
340conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum_with_scalar_mult
341instantiation432, 406, 378  ⊢  
  : , : , :
342instantiation379, 558, 410  ⊢  
  : , : , : , : , : , :
343generalization380  ⊢  
344conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation_with_scalar_mult
345modus ponens381, 382,  ⊢  
346instantiation559, 507, 558  ⊢  
  : , : , :
347conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
348instantiation559, 515, 383  ⊢  
  : , : , :
349instantiation473, 451  ⊢  
  :
350instantiation495  ⊢  
  : , :
351instantiation559, 521, 384  ⊢  
  : , : , :
352conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
353conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat3
354instantiation385  ⊢  
  : , : , :
355conjecture  ⊢  
 proveit.numbers.exponentiation.sqrt_real_pos_closure
356instantiation559, 530, 386,  ⊢  
  : , : , :
357conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonneg_difference
358instantiation387, 551  ⊢  
  :
359conjecture  ⊢  
 proveit.numbers.ordering.less_shift_add_right
360instantiation388, 421, 389, 390, 391  ⊢  
  : , : , :
361instantiation392, 546, 555, 427, 479, 393, 481, 429, 456  ⊢  
  : , : , : , : , : , :
362instantiation394, 456, 481  ⊢  
  : , :
363instantiation557, 551  ⊢  
  :
364conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_basic
365instantiation495  ⊢  
  : , :
366instantiation559, 521, 395  ⊢  
  : , : , :
367conjecture  ⊢  
 proveit.numbers.negation.double_negation
368instantiation559, 521, 396  ⊢  
  : , : , :
369instantiation425, 397, 398*  ⊢  
  : , :
370axiom  ⊢  
 proveit.logic.equality.equals_transitivity
371instantiation459, 399  ⊢  
  : , : , :
372instantiation425, 400  ⊢  
  : , :
373instantiation401, 402, 403,  ⊢  
  : , : , :
374instantiation404, 561, 540,  ⊢  
  : , :
375instantiation424, 445, 406,  ⊢  
  : , :
376conjecture  ⊢  
 proveit.core_expr_types.lambda_maps.general_lambda_substitution
377instantiation405, 546, 427, 479, 406, 445,  ⊢  
  : , : , : , : , : , :
378instantiation407  ⊢  
  :
379conjecture  ⊢  
 proveit.linear_algebra.addition.summation_closure
380instantiation443, 410, 445, 408,  ⊢  
  : , : , : , :
381instantiation409, 445, 427, 546, 410, 479,  ⊢  
  : , : , : , : , : , : , : , :
382instantiation437, 538, 441, 442, 444, 411, 439, 412,  ⊢  
  : , : , : , :
383instantiation413, 421, 414  ⊢  
  : , :
384instantiation559, 530, 415  ⊢  
  : , : , :
385conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
386instantiation559, 534, 416,  ⊢  
  : , : , :
387conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
388conjecture  ⊢  
 proveit.numbers.exponentiation.exponential_monotonocity
389instantiation559, 450, 486  ⊢  
  : , : , :
390instantiation559, 450, 417  ⊢  
  : , : , :
391instantiation418, 451  ⊢  
  :
392conjecture  ⊢  
 proveit.numbers.addition.disassociation
393instantiation495  ⊢  
  : , :
394conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
395instantiation473, 496  ⊢  
  :
396instantiation559, 530, 419  ⊢  
  : , : , :
397instantiation461, 538, 420, 421, 422, 456, 423*  ⊢  
  : , : , :
398instantiation424, 481, 502  ⊢  
  : , :
399instantiation425, 426  ⊢  
  : , :
400instantiation475, 546, 555, 427, 479, 428, 502, 429, 481, 430*, 431*  ⊢  
  : , : , : , : , : , :
401theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
402instantiation432, 433, 434,  ⊢  
  : , : , :
403instantiation435, 506, 481,  ⊢  
  : , :
404conjecture  ⊢  
 proveit.physics.quantum.algebra.prepend_num_ket_with_one_ket
405conjecture  ⊢  
 proveit.numbers.multiplication.association
406instantiation559, 465, 436  ⊢  
  : , : , :
407conjecture  ⊢  
 proveit.numbers.multiplication.unary_mult_reduction
408instantiation437, 538, 441, 442, 444, 438, 439, 446,  ⊢  
  : , : , : , :
409conjecture  ⊢  
 proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
410instantiation440, 538, 441, 442, 444  ⊢  
  : , : , :
411instantiation495  ⊢  
  : , :
412instantiation443, 444, 445, 446,  ⊢  
  : , : , : , :
413conjecture  ⊢  
 proveit.numbers.exponentiation.exp_real_pos_closure
414instantiation559, 530, 447  ⊢  
  : , : , :
415conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.zero_is_rational
416instantiation559, 550, 448,  ⊢  
  : , : , :
417instantiation559, 507, 511  ⊢  
  : , : , :
418conjecture  ⊢  
 proveit.numbers.ordering.less_than_successor
419instantiation559, 534, 449  ⊢  
  : , : , :
420instantiation495  ⊢  
  : , :
421instantiation559, 450, 487  ⊢  
  : , : , :
422instantiation559, 521, 451  ⊢  
  : , : , :
423instantiation452, 502  ⊢  
  :
424conjecture  ⊢  
 proveit.numbers.multiplication.commutation
425theorem  ⊢  
 proveit.logic.equality.equals_reversal
426instantiation453, 481  ⊢  
  :
427theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
428instantiation495  ⊢  
  : , :
429instantiation559, 521, 454  ⊢  
  : , : , :
430instantiation455, 456, 502, 457  ⊢  
  : , : , :
431instantiation458, 481  ⊢  
  :
432theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
433instantiation459, 460,  ⊢  
  : , : , :
434instantiation461, 538, 462, 516, 484, 463,  ⊢  
  : , : , :
435conjecture  ⊢  
 proveit.numbers.addition.commutation
436instantiation482, 483, 463  ⊢  
  : , :
437conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
438instantiation495  ⊢  
  : , :
439conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_one_in_qubit_space
440conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
441instantiation495  ⊢  
  : , :
442instantiation464, 538  ⊢  
  :
443conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
444instantiation464, 551  ⊢  
  :
445instantiation559, 465, 466,  ⊢  
  : , : , :
446instantiation467, 561, 540,  ⊢  
  : , :
447instantiation559, 468, 469  ⊢  
  : , : , :
448instantiation554, 555, 470,  ⊢  
  : , :
449instantiation559, 550, 471  ⊢  
  : , : , :
450conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
451instantiation559, 530, 472  ⊢  
  : , : , :
452conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
453conjecture  ⊢  
 proveit.numbers.negation.mult_neg_one_left
454instantiation473, 474  ⊢  
  :
455conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
456instantiation559, 521, 474  ⊢  
  : , : , :
457conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
458conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
459axiom  ⊢  
 proveit.logic.equality.substitution
460instantiation475, 476, 555, 546, 477, 478, 479, 502, 503, 504, 505, 506, 481,  ⊢  
  : , : , : , : , : , :
461conjecture  ⊢  
 proveit.numbers.exponentiation.products_of_complex_powers
462instantiation495  ⊢  
  : , :
463instantiation499, 500, 480, 502, 503, 504, 505, 481  ⊢  
  : , :
464conjecture  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
465conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.complex_nonzero_within_complex
466instantiation482, 483, 484,  ⊢  
  : , :
467conjecture  ⊢  
 proveit.physics.quantum.algebra.num_ket_in_register_space
468conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
469instantiation485, 486, 487  ⊢  
  : , :
470instantiation488, 489,  ⊢  
  :
471instantiation554, 555, 490  ⊢  
  : , :
472instantiation559, 534, 491  ⊢  
  : , : , :
473conjecture  ⊢  
 proveit.numbers.negation.real_closure
474instantiation492, 493, 558  ⊢  
  : , : , :
475conjecture  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
476conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat4
477instantiation494  ⊢  
  : , : , : , :
478instantiation495  ⊢  
  : , :
479conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
480instantiation517  ⊢  
  : , : , : , : , :
481instantiation559, 521, 496  ⊢  
  : , : , :
482conjecture  ⊢  
 proveit.numbers.exponentiation.exp_complex_nonzero_closure
483instantiation559, 497, 498  ⊢  
  : , : , :
484instantiation499, 500, 501, 502, 503, 504, 505, 506,  ⊢  
  : , :
485conjecture  ⊢  
 proveit.numbers.division.div_rational_pos_closure
486instantiation559, 507, 561  ⊢  
  : , : , :
487instantiation559, 507, 538  ⊢  
  : , : , :
488conjecture  ⊢  
 proveit.numbers.negation.nat_closure
489instantiation508, 509, 510,  ⊢  
  :
490instantiation559, 560, 511  ⊢  
  : , : , :
491instantiation559, 550, 561  ⊢  
  : , : , :
492theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
493instantiation512, 513  ⊢  
  : , :
494conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
495conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
496instantiation559, 530, 514  ⊢  
  : , : , :
497conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
498instantiation559, 515, 516  ⊢  
  : , : , :
499conjecture  ⊢  
 proveit.numbers.multiplication.mult_complex_closure
500conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat5
501instantiation517  ⊢  
  : , : , : , : , :
502instantiation559, 521, 518  ⊢  
  : , : , :
503instantiation559, 521, 519  ⊢  
  : , : , :
504conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
505instantiation559, 521, 520  ⊢  
  : , : , :
506instantiation559, 521, 522,  ⊢  
  : , : , :
507conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
508conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
509instantiation559, 523, 525,  ⊢  
  : , : , :
510instantiation524, 532, 543, 525,  ⊢  
  : , : , :
511instantiation526, 561, 558  ⊢  
  : , :
512theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
513conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
514instantiation559, 534, 548  ⊢  
  : , : , :
515conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
516conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
517conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
518instantiation559, 530, 527  ⊢  
  : , : , :
519instantiation559, 528, 529  ⊢  
  : , : , :
520conjecture  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
521conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
522instantiation559, 530, 531,  ⊢  
  : , : , :
523instantiation542, 532, 543  ⊢  
  : , :
524conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
525assumption  ⊢  
526conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
527instantiation559, 534, 533  ⊢  
  : , : , :
528conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
529conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
530conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
531instantiation559, 534, 535,  ⊢  
  : , : , :
532instantiation547, 536, 537  ⊢  
  : , :
533instantiation559, 550, 538  ⊢  
  : , : , :
534conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
535instantiation559, 539, 540,  ⊢  
  : , : , :
536instantiation559, 552, 541  ⊢  
  : , : , :
537instantiation559, 550, 558  ⊢  
  : , : , :
538conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat2
539instantiation542, 543, 544  ⊢  
  : , :
540assumption  ⊢  
541instantiation557, 561  ⊢  
  :
542conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
543instantiation559, 545, 546  ⊢  
  : , : , :
544instantiation547, 548, 549  ⊢  
  : , :
545conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
546axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
547conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
548instantiation559, 550, 551  ⊢  
  : , : , :
549instantiation559, 552, 553  ⊢  
  : , : , :
550conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
551instantiation554, 555, 556  ⊢  
  : , :
552conjecture  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
553instantiation557, 558  ⊢  
  :
554conjecture  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
555theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
556instantiation559, 560, 561  ⊢  
  : , : , :
557conjecture  ⊢  
 proveit.numbers.negation.int_neg_closure
558conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
559theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
560conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
561assumption  ⊢  
*equality replacement requirements